Inference at * 1 1 4 2 1 
Iof proof for Lemma gen hyp tp:



1. A : Type
2. e : A
3. H : AType
4. x : A
5. e = x
6. z : H(e)
7. A  Type
8. e  A
9. x:A. (e = x)  Type
  z  0 

latex

 by (\p.let A = get_term_arg `A` p 
 bin let x = get_term_arg `x` p 

 binin let e = get_term_arg `e` p 
 bin 
 biAt (get_term_arg `UH` p) 
 bi(Subst 
 bi(Sub(
 mk_equal_term 
 mk_equa(mk_set_term (dv x) A (mk_equal_term A e x)) 
 mk_equae 
 mk_equax) 

 mk_equax(get_int_arg `i` p + 2)) p) 

latex

 1: 

 1: 6. z : H(x)
 1: 7. A  Type
 1: 8. e  A
 1: 9. x:A. (e = x)  Type
 1:   z  0
 2: .....wf..... NILNIL

 2:   z1:{x:A| e = x} . H(z1)  Type
 3: .....equality..... NILNIL

 3:   e = x
 .

Definitions

t  T, x:A. B(x)